CopatternsSplitErrorWithUnboundDBIndex.agda:20,1-15
Cannot eliminate type  A → A → A × A  with projection  fst
when checking that the clause fst test a = a has type
{A B : Set} → A → A → A × A
